COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002		outline
C00005 00003	There is a large area of contemporary mathematics which can be profitably
C00006 00004	
C00007 ENDMK
C⊗;
	outline

description of existing system
 input/output format
 on-line features
 compare with others
  Bledsoe  -for natural i/o
  Guard    -for on-line
  Wos & ?  -for strategy lang.
  Nevins   -for ?
 don't say much about insides- not relevant.

examples
 marsden: verif
 geometry:explor
 tba:     verif 
 cowan:   verif and explor
 houses:  prog.lang.  (c.f. jfs disjunctions)

general discussion of existing system
 what's good
  natural i/0
   better than B&B
  partitioning, but should be broadened
 what's bad
  subproblem control--general control problem
   getting instantiations back
  must be able to express intuitions in terms of control

applications
 simple mathematics -desk calculator
 intuition builder  -for beginner

conclusions
 tp. like this one are limited
  is resolution the way?
 completeness downplayed
  work this back into discussion of examples
 incompleteness manifestation:
   in the strategies
   in the use of on-line
 ever used completeness in positive way? i.e. "no-proof found" => ... .
 key issue: logic validity of rules 
            computationally sound (don't take forever?)

extensions
 how about typing and a.d.s.?
 languages for tp.
  description of primitives -substitution, application
  control structures  -reasonably wild control: suspend, resume, kill, ...
  data structures
  attempt to discover by looking at examples (ours and Bledsoe and Bruell)
    also look at prove1.new in abstract form.
  how about induction: goal structure?
There is a large area of contemporary mathematics which can be profitably
explored using an interactive first-order theorem prover.  This report
will describe #   applications of the the Stanford A.I. Project's theorem prover. 

The first application explores the field of Euclidean Geometry.  
The second example deals with abstract algebra, in particular, Implicative models.
Third, we used some of the programmable features of the prover to give a solution 
to a puzzle.